Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.


↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

old(serve) → free(serve)
Used ordering:
Polynomial interpretation [25]:

POL(check(x1)) = x1   
POL(free(x1)) = x1   
POL(new(x1)) = x1   
POL(old(x1)) = 2·x1   
POL(serve) = 2   
POL(top(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

old(free(x)) → free(old(x))
Used ordering:
Polynomial interpretation [25]:

POL(check(x1)) = x1   
POL(free(x1)) = 1 + x1   
POL(new(x1)) = 1 + x1   
POL(old(x1)) = 2·x1   
POL(serve) = 0   
POL(top(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

check(old(x)) → old(check(x))
check(old(x)) → old(x)
Used ordering:
Polynomial interpretation [25]:

POL(check(x1)) = 2·x1   
POL(free(x1)) = 2·x1   
POL(new(x1)) = x1   
POL(old(x1)) = 2 + x1   
POL(serve) = 0   
POL(top(x1)) = x1   




↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TOP(free(x)) → TOP(check(new(x)))
CHECK(free(x)) → CHECK(x)
TOP(free(x)) → CHECK(new(x))
TOP(free(x)) → NEW(x)
CHECK(new(x)) → CHECK(x)
CHECK(new(x)) → NEW(check(x))
NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x)) → TOP(check(new(x)))
CHECK(free(x)) → CHECK(x)
TOP(free(x)) → CHECK(new(x))
TOP(free(x)) → NEW(x)
CHECK(new(x)) → CHECK(x)
CHECK(new(x)) → NEW(check(x))
NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 3 less nodes.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

NEW(free(x)) → NEW(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

NEW(free(x)) → NEW(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                      ↳ QDP
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

NEW(free(x)) → NEW(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

NEW(free(x)) → NEW(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(NEW(x1)) = 2·x1   
POL(free(x1)) = 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                      ↳ QDP
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

CHECK(free(x)) → CHECK(x)
CHECK(new(x)) → CHECK(x)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(CHECK(x1)) = 2·x1   
POL(free(x1)) = 2·x1   
POL(new(x1)) = 2·x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ UsableRulesReductionPairsProof
                              ↳ QDP
                                ↳ PisEmptyProof
                      ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(free(x)) → TOP(check(new(x))) at position [0] we obtained the following new rules:

TOP(free(x0)) → TOP(new(check(x0)))
TOP(free(free(x0))) → TOP(check(free(new(x0))))
TOP(free(serve)) → TOP(check(free(serve)))



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ QDPOrderProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x0)) → TOP(new(check(x0)))
TOP(free(free(x0))) → TOP(check(free(new(x0))))
TOP(free(serve)) → TOP(check(free(serve)))

The TRS R consists of the following rules:

new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


TOP(free(serve)) → TOP(check(free(serve)))
The remaining pairs can at least be oriented weakly.

TOP(free(x0)) → TOP(new(check(x0)))
TOP(free(free(x0))) → TOP(check(free(new(x0))))
Used ordering: Polynomial Order [21,25] with Interpretation:

POL( check(x1) ) = max{0, -1}


POL( TOP(x1) ) = x1 + 1


POL( new(x1) ) = x1


POL( serve ) = 1


POL( free(x1) ) = x1



The following usable rules [17] were oriented:

check(new(x)) → new(check(x))
new(free(x)) → free(new(x))
check(free(x)) → free(check(x))
new(serve) → free(serve)



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ SemLabProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x0)) → TOP(new(check(x0)))
TOP(free(free(x0))) → TOP(check(free(new(x0))))

The TRS R consists of the following rules:

new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.check: 1
new: x0
TOP: 0
serve: 0
free: x0
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

TOP.1(free.1(free.1(x0))) → TOP.1(check.1(free.1(new.1(x0))))
TOP.1(free.1(x0)) → TOP.1(new.1(check.1(x0)))
TOP.0(free.0(x0)) → TOP.1(new.1(check.0(x0)))
TOP.0(free.0(free.0(x0))) → TOP.1(check.0(free.0(new.0(x0))))

The TRS R consists of the following rules:

check.0(new.0(x)) → new.1(check.0(x))
check.1(new.1(x)) → new.1(check.1(x))
new.1(free.1(x)) → free.1(new.1(x))
check.0(free.0(x)) → free.1(check.0(x))
check.1(free.1(x)) → free.1(check.1(x))
new.0(serve.) → free.0(serve.)
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ SemLabProof
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP.1(free.1(free.1(x0))) → TOP.1(check.1(free.1(new.1(x0))))
TOP.1(free.1(x0)) → TOP.1(new.1(check.1(x0)))
TOP.0(free.0(x0)) → TOP.1(new.1(check.0(x0)))
TOP.0(free.0(free.0(x0))) → TOP.1(check.0(free.0(new.0(x0))))

The TRS R consists of the following rules:

check.0(new.0(x)) → new.1(check.0(x))
check.1(new.1(x)) → new.1(check.1(x))
new.1(free.1(x)) → free.1(new.1(x))
check.0(free.0(x)) → free.1(check.0(x))
check.1(free.1(x)) → free.1(check.1(x))
new.0(serve.) → free.0(serve.)
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ SemLabProof
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ UsableRulesReductionPairsProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP.1(free.1(free.1(x0))) → TOP.1(check.1(free.1(new.1(x0))))
TOP.1(free.1(x0)) → TOP.1(new.1(check.1(x0)))

The TRS R consists of the following rules:

check.0(new.0(x)) → new.1(check.0(x))
check.1(new.1(x)) → new.1(check.1(x))
new.1(free.1(x)) → free.1(new.1(x))
check.0(free.0(x)) → free.1(check.0(x))
check.1(free.1(x)) → free.1(check.1(x))
new.0(serve.) → free.0(serve.)
new.0(free.0(x)) → free.0(new.0(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

TOP.1(free.1(free.1(x0))) → TOP.1(check.1(free.1(new.1(x0))))
TOP.1(free.1(x0)) → TOP.1(new.1(check.1(x0)))
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(TOP.1(x1)) = x1   
POL(check.1(x1)) = x1   
POL(free.1(x1)) = 1 + x1   
POL(new.1(x1)) = x1   



↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ QDPOrderProof
                                  ↳ QDP
                                    ↳ SemLabProof
                                      ↳ QDP
                                        ↳ DependencyGraphProof
                                          ↳ QDP
                                            ↳ UsableRulesReductionPairsProof
                                              ↳ QDP
                                                ↳ PisEmptyProof
                        ↳ UsableRulesProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
P is empty.
The TRS R consists of the following rules:

check.1(new.1(x)) → new.1(check.1(x))
check.1(free.1(x)) → free.1(check.1(x))
new.1(free.1(x)) → free.1(new.1(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ RRRPoloQTRSProof
        ↳ QTRS
          ↳ RRRPoloQTRSProof
            ↳ QTRS
              ↳ DependencyPairsProof
                ↳ QDP
                  ↳ DependencyGraphProof
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                        ↳ UsableRulesProof
                          ↳ QDP
  ↳ QTRS Reverse
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

TOP(free(x)) → TOP(check(new(x)))

The TRS R consists of the following rules:

new(free(x)) → free(new(x))
new(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

The set Q is empty.
We have obtained the following QTRS:

free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
serve'(old(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)

The set Q is empty.

↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
    ↳ QTRS
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
serve'(old(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)

Q is empty.

We have reversed the following QTRS:
The set of rules R is

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

The set Q is empty.
We have obtained the following QTRS:

free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
serve'(old(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)

The set Q is empty.

↳ QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
  ↳ QTRS Reverse
    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

free(top(x)) → new(check(top(x)))
free(new(x)) → new(free(x))
free(old(x)) → old(free(x))
serve'(new(x)) → serve'(free(x))
serve'(old(x)) → serve'(free(x))
free(check(x)) → check(free(x))
new(check(x)) → check(new(x))
old(check(x)) → check(old(x))
old(check(x)) → old(x)

Q is empty.